These days we can let GitHub update stage0, which I find a bit cleaner. Should we trigger a stage0 update on master and only the workaround needs to be PRed then, or is that for some reason not desirable here?

@nomeata it would be desirable, I just couldn't figure out how to do it! It looked like #3042 only runs if stdlib_flags.h has changed which is not the case here.

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-21 11:27:43)
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-22' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-22 14:55:39)

It can only be done by people with write permissions. Started at https://github.com/leanprover/lean4/actions/runs/7287788936, let’s see if this works (this is rather new)

We will merge this, but I'll also cherry-pick the release notes onto the release/v4.5.0 branch when I start that tomorrow.

@Vtec234, done, you can merge latest master into this.